Sequent and Hypersequent Calculi for Abelian and Lukasiewicz Logics

摘要

We present two embeddings of infinite-valued Lukasiewicz logic L into Meyerand Slaney's abelian logic A, the logic of lattice-ordered abelian groups. Wegive new analytic proof systems for A and use the embeddings to derivecorresponding systems for L. These include: hypersequent calculi for A and Land terminating versions of these calculi; labelled single sequent calculi forA and L of complexity co-NP; unlabelled single sequent calculi for A and L.